Inference at * 2 1 
Iof proof for Lemma p-fun-exp-compose:



1. T : Type
2. n : 
3. 0 < n
4. h, f:(T(T + Top)). f^n - 1 o h   = primrec(n - 1;h;i,g. f o g  )
5. h : T(T + Top)
6. f : T(T + Top)
  primrec(1+(n - 1);p-id();i,g. f o g  ) o h   = f o primrec(n - 1;h;i,g. f o g  )   

latex

 by Subst primrec(1+(n - 1);p-id();i,g. f o g  ) = f o primrec(n - 1;p-id();i,g. f o g  )  
 b0 THEN Auto 

latex

 1: .....equality..... NILNIL

 1:   primrec(1+(n - 1);p-id();i,g. f o g  ) = f o primrec(n - 1;p-id();i,g. f o g  )  
 2: 

 2:   f o primrec(n - 1;p-id();i,g. f o g  )   o h   = f o primrec(n - 1;h;i,g. f o g  )  
 .

Definitions	s = t, x:AB(x), left + right, Top, n+m, primrec(n;b;c), n - m, #$n, p-id(), x.A(x), f o g  , , x:A. B(x), t  T
Lemmas	p-compose wf